SherbyNet - /page/wikibook/entry.mu

Micron Document

<!DOCTYPE html>

<title>Set constraint</title>

</head>

Set constraint

</h1>

</header>

/* start https://en.wikipedia.org/ */

.mw-parser-output .ambox{border:1px solid #a2a9b1;border-left:10px solid #36c;background-color:#fbfbfb;box-sizing:border-box}.mw-parser-output .ambox+link+.ambox,.mw-parser-output .ambox+link+style+.ambox,.mw-parser-output .ambox+link+link+.ambox,.mw-parser-output .ambox+.mw-empty-elt+link+.ambox,.mw-parser-output .ambox+.mw-empty-elt+link+style+.ambox,.mw-parser-output .ambox+.mw-empty-elt+link+link+.ambox{margin-top:-1px}html body.mediawiki .mw-parser-output .ambox.mbox-small-left{margin:4px 1em 4px 0;overflow:hidden;width:238px;border-collapse:collapse;font-size:88%;line-height:1.25em}.mw-parser-output .ambox-speedy{border-left:10px solid #b32424;background-color:#fee7e6}.mw-parser-output .ambox-delete{border-left:10px solid #b32424}.mw-parser-output .ambox-content{border-left:10px solid #f28500}.mw-parser-output .ambox-style{border-left:10px solid #fc3}.mw-parser-output .ambox-move{border-left:10px solid #9932cc}.mw-parser-output .ambox-protection{border-left:10px solid #a2a9b1}.mw-parser-output .ambox .mbox-text{border:none;padding:0.25em 0.5em;width:100%}.mw-parser-output .ambox .mbox-image{border:none;padding:2px 0 2px 0.5em;text-align:center}.mw-parser-output .ambox .mbox-imageright{border:none;padding:2px 0.5em 2px 0;text-align:center}.mw-parser-output .ambox .mbox-empty-cell{border:none;padding:0;width:1px}.mw-parser-output .ambox .mbox-image-div{width:52px}@media(min-width:720px){.mw-parser-output .ambox{margin:0 10%}}@media print{body.ns-0 .mw-parser-output .ambox{display:none!important}}

/* end https://en.wikipedia.org/ */

</style>

In <a href="Mathematics" title="Mathematics">mathematics</a> and <a href="Theoretical_computer_science" title="Theoretical computer science">theoretical computer science</a>, a set constraint is an equation or an inequation between sets of <a href="Term_(logic)#Formal_definition" title="Term (logic)">terms</a>.

Similar to systems of (<a href="Inequation#Solving_inequations" title="Inequation">in</a>)<a href="Equation_solving" title="Equation solving">equations</a> between numbers, methods are studied for solving systems of set constraints.

Different approaches admit different operators (like "∪", "∩", "\", and function application)<a href="#cite_note-1">[note 1]</a> on sets and different (in)equation relations (like "=", "⊆", and "⊈") between set expressions.

Systems of set constraints are useful to describe (in particular infinite) sets of <a href="Ground_term" class="mw-redirect" title="Ground term">ground terms</a>.<a href="#cite_note-2">[note 2]</a>

They arise in program analysis, <a href="Abstract_interpretation" title="Abstract interpretation">abstract interpretation</a>, and <a href="Type_inference" title="Type inference">type inference</a>.

<div class="mw-heading mw-heading2"><h2 id="Relation_to_regular_tree_grammars">Relation to regular tree grammars</h2></div>

Each <a href="Regular_tree_grammar" title="Regular tree grammar">regular tree grammar</a> can be systematically transformed into a system of set inclusions such that its minimal solution corresponds to the tree language of the grammar.

For example, the grammar (terminal and nonterminal symbols indicated by lower and upper case initials, respectively) with the rules

<td>BoolG</td>

<td>→ false

</td></tr>

<tr>

<td>BoolG</td>

<td>→ true

</td></tr>

<tr>

<td>BListG</td>

<td>→ nil

</td></tr>

<tr>

<td>BListG</td>

<td>→ cons(BoolG,BListG)

</td></tr>

<tr>

<td>BList1G</td>

<td>→ cons(true,BListG)

</td></tr>

<tr>

<td>BList1G</td>

<td>→ cons(false,BList1G)

</td></tr></tbody></table></dd></dl>

is transformed to the set inclusion system (constants and variables indicated by lower and upper case initials, respectively):

<td>BoolS</td>

<td>⊇ false

</td></tr>

<tr>

<td>BoolS</td>

<td>⊇ true

</td></tr>

<tr>

<td>BListS</td>

<td>⊇ nil

</td></tr>

<tr>

<td>BListS</td>

<td>⊇ cons(BoolS,BListS)

</td></tr>

<tr>

<td>BList1S</td>

<td>⊇ cons(true,BListS)

</td></tr>

<tr>

<td>BList1S</td>

<td>⊇ cons(false,BList1S)

</td></tr></tbody></table></dd></dl>

This system has a minimal solution, viz. ("L(N)" denoting the tree language corresponding to the nonterminal N in the above tree grammar):

<td>BoolS</td>

<td>= L(BoolG)</td>

<td>= { false, true }

</td></tr>

<tr>

<td>BListS</td>

<td>= L(BListG)</td>

<td>= { nil, cons(false,nil), cons(true,nil), cons(false,cons(false,nil)), ... }

</td></tr>

<tr>

<td>BList1S</td>

<td>= L(BList1G)</td>

<td>= { nil, cons(true,nil), cons(true,cons(false,nil)),... }

</td></tr></tbody></table></dd></dl>

The maximal solution of the system is trivial; it assigns the set of all terms to every variable.

<div class="mw-heading mw-heading2"><h2 id="Literature">Literature</h2></div>

/* start https://en.wikipedia.org/ */

.mw-parser-output cite.citation{font-style:inherit;word-wrap:break-word}.mw-parser-output .citation q{quotes:"\"""\"""'""'"}.mw-parser-output .citation:target{background-color:rgba(0,127,255,0.133)}.mw-parser-output .id-lock-free.id-lock-free a{background:url("./mw/Lock-green.svg")right 0.1em center/9px no-repeat}.mw-parser-output .id-lock-limited.id-lock-limited a,.mw-parser-output .id-lock-registration.id-lock-registration a{background:url("./mw/Lock-gray-alt-2.svg")right 0.1em center/9px no-repeat}.mw-parser-output .id-lock-subscription.id-lock-subscription a{background:url("./mw/Lock-red-alt-2.svg")right 0.1em center/9px no-repeat}.mw-parser-output .cs1-ws-icon a{background:url("./mw/Wikisource-logo.svg")right 0.1em center/12px no-repeat}body:not(.skin-timeless):not(.skin-minerva) .mw-parser-output .id-lock-free a,body:not(.skin-timeless):not(.skin-minerva) .mw-parser-output .id-lock-limited a,body:not(.skin-timeless):not(.skin-minerva) .mw-parser-output .id-lock-registration a,body:not(.skin-timeless):not(.skin-minerva) .mw-parser-output .id-lock-subscription a,body:not(.skin-timeless):not(.skin-minerva) .mw-parser-output .cs1-ws-icon a{background-size:contain;padding:0 1em 0 0}.mw-parser-output .cs1-code{color:inherit;background:inherit;border:none;padding:inherit}.mw-parser-output .cs1-hidden-error{display:none;color:var(--color-error,#d33)}.mw-parser-output .cs1-visible-error{color:var(--color-error,#d33)}.mw-parser-output .cs1-maint{display:none;color:#085;margin-left:0.3em}.mw-parser-output .cs1-kern-left{padding-left:0.2em}.mw-parser-output .cs1-kern-right{padding-right:0.2em}.mw-parser-output .citation .mw-selflink{font-weight:inherit}@media screen{.mw-parser-output .cs1-format{font-size:95%}html.skin-theme-clientpref-night .mw-parser-output .cs1-maint{color:#18911f}}@media screen and (prefers-color-scheme:dark){html.skin-theme-clientpref-os .mw-parser-output .cs1-maint{color:#18911f}}

/* end https://en.wikipedia.org/ */

</style><cite id="CITEREFAiken,_A.1995" class="citation techreport cs1">Aiken, A. (1995). <a rel="nofollow" class="external text" href="http://citeseer.uark.edu:8080/citeseerx/viewdoc/summary;jsessionid=01CAFC5839497EE6030F707B5B5C9CAA?doi=10.1.1.47.537">Set Constraints: Results, Applications and Future Directions</a> (Technical report). Univ. Berkeley.</cite></li>

<li><cite id="CITEREFAiken,_A.,_Kozen,_D.,_Vardi,_M.,_Wimmers,_E.L.1993" class="citation techreport cs1">Aiken, A., Kozen, D., Vardi, M., Wimmers, E.L. (May 1993). <a rel="nofollow" class="external text" href="http://theory.stanford.edu/~aiken/publications/papers/csl93.ps">The Complexity of Set Constraints</a> (Technical report). Computer Science Department, Cornell University. 93–1352.</cite><code class="cs1-code">{{cite tech report}}</code>: CS1 maint: multiple names: authors list (link)</li>

<li><cite id="CITEREFAiken,_A.,_Kozen,_D.,_Vardi,_M.,_Wimmers,_E.L.1994" class="citation book cs1">Aiken, A., Kozen, D., Vardi, M., Wimmers, E.L. (1994). "The Complexity of Set Constraints". Computer Science Logic'93. LNCS. Vol. 832. Springer. pp. 1–17.</cite><code class="cs1-code">{{cite book}}</code>: CS1 maint: multiple names: authors list (link)</li>

<li><cite id="CITEREFAiken,_A.,_Wimmers,_E.L.1992" class="citation book cs1">Aiken, A., Wimmers, E.L. (1992). "Solving Systems of Set Constraints (Extended Abstract)". Seventh Annual IEEE Symposium on Logic in Computer Science. pp. 329–340.</cite><code class="cs1-code">{{cite book}}</code>: CS1 maint: multiple names: authors list (link)</li>

<li><cite id="CITEREFBachmair,_Leo,_Ganzinger,_Harald,_Waldmann,_Uwe1992" class="citation techreport cs1">Bachmair, Leo, Ganzinger, Harald, Waldmann, Uwe (1992). Set Constraints are the Monadic Class (Technical report). Max-Planck-Institut für Informatik. p. 13. <a href="CiteSeerX_(identifier)" class="mw-redirect" title="CiteSeerX (identifier)">CiteSeerX</a> <a rel="nofollow" class="external text" href="https://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.32.3739">10.1.1.32.3739</a>. MPI-I-92-240.</cite><code class="cs1-code">{{cite tech report}}</code>: CS1 maint: multiple names: authors list (link)</li>

<li><cite id="CITEREFBachmair,_Leo,_Ganzinger,_Harald,_Waldmann,_Uwe1993" class="citation book cs1">Bachmair, Leo, Ganzinger, Harald, Waldmann, Uwe (1993). "Set Constraints are the Monadic Class". Eight Annual IEEE Symposium on Logic in Computer Science. pp. 75–83.</cite><code class="cs1-code">{{cite book}}</code>: CS1 maint: multiple names: authors list (link)</li>

<li><cite id="CITEREFCharatonik,_W.1994" class="citation book cs1">Charatonik, W. (Sep 1994). "Set Constraints in Some Equational Theories". Proc. 1st Int. Conf. on Constraints in Computational Logics (CCL). LNCS. Vol. 845. Springer. pp. 304–319.</cite></li>

<li><cite id="CITEREFCharatonikPodelski2002" class="citation journal cs1">Charatonik, Witold; Podelski, Andreas (2002). <a rel="nofollow" class="external text" href="https://doi.org/10.1006%2Finco.2001.2952">"Set Constraints with Intersection"</a>. Information and Computation. 179 (2): 213–229. <a href="Doi_(identifier)" class="mw-redirect" title="Doi (identifier)">doi</a>:<a rel="nofollow" class="external text" href="https://doi.org/10.1006%2Finco.2001.2952">10.1006/inco.2001.2952</a>.</cite></li>

<li><cite id="CITEREFCharatonik,_W.,_Podelski,_A.1998" class="citation book cs1">Charatonik, W., Podelski, A. (1998). <a href="Tobias_Nipkow" title="Tobias Nipkow">Tobias Nipkow</a> (ed.). Co-definite Set Constraints. LNCS 1379. Springer-Verlag. pp. 211–225.</cite><code class="cs1-code">{{cite book}}</code>: CS1 maint: multiple names: authors list (link)</li>

<li><cite id="CITEREFCharatonik,_W.,_Talbot,_J.-M.2002" class="citation book cs1">Charatonik, W., Talbot, J.-M. (2002). Tison, S. (ed.). Atomic Set Constraints with Projection. LNCS 2378. Springer. pp. 311–325.</cite><code class="cs1-code">{{cite book}}</code>: CS1 maint: multiple names: authors list (link)</li>

<li><cite id="CITEREFGilleron,_R.,_Tison,_S.,_Tommasi,_M.1993" class="citation book cs1">Gilleron, R., Tison, S., Tommasi, M. (1993). "Solving Systems of Set Constraints using Tree Automata". 10th Annual Symposium on Theoretical Aspects of Computer Science. LNCS. Vol. 665. Springer. pp. 505–514.</cite><code class="cs1-code">{{cite book}}</code>: CS1 maint: multiple names: authors list (link)</li>

<li><cite id="CITEREFHeintze,_N.,_Jaffar,_J.1990" class="citation book cs1">Heintze, N., Jaffar, J. (1990). "A Decision Procedure for a Class of Set Constraints (Extended Abstract)". Fifth Annual IEEE Symposium on Logic in Computer Science. pp. 42–51.</cite><code class="cs1-code">{{cite book}}</code>: CS1 maint: multiple names: authors list (link)</li>

<li><cite id="CITEREFHeintze,_N.,_Jaffar,_J.1991" class="citation techreport cs1">Heintze, N., Jaffar, J. (Feb 1991). A Decision Procedure for a Class of Set Constraints (Technical report). School of Computer Science, Carnegie Mellon University.</cite><code class="cs1-code">{{cite tech report}}</code>: CS1 maint: multiple names: authors list (link)</li>

<li><cite id="CITEREFKozen,_D.1993" class="citation book cs1">Kozen, D. (1993). <a rel="nofollow" class="external text" href="http://www.cs.cornell.edu/~kozen/papers/lasc.pdf">"Logical Aspects of Set Constraints"</a> (PDF). Computer Science Logic'93. LNCS. Vol. 832. pp. 175–188.</cite></li>

<li><cite id="CITEREFKozen,_D.1994" class="citation book cs1">Kozen, D. (1994). "Set Constraints and Logic Programming". CCL. LNCS. Vol. 845.</cite></li>

<li><cite id="CITEREFDexter_Kozen1998" class="citation journal cs1">Dexter Kozen (1998). <a rel="nofollow" class="external text" href="https://doi.org/10.1006%2Finco.1997.2694">"Set Constraints and Logic Programming"</a>. Information and Computation. 142: 2–25. <a href="Doi_(identifier)" class="mw-redirect" title="Doi (identifier)">doi</a>:<a rel="nofollow" class="external text" href="https://doi.org/10.1006%2Finco.1997.2694">10.1006/inco.1997.2694</a>.</cite></li>

<li><cite id="CITEREFUribe,_T.E.1992" class="citation book cs1">Uribe, T.E. (1992). <a rel="nofollow" class="external text" href="http://theory.stanford.edu/~uribe/papers/unification.ps.Z">"Sorted Unification Using Set Constraints"</a>. Proc. CADE–11. LNCS. Vol. 607. pp. 163–177.</cite></li></ul>

<div class="mw-heading mw-heading3"><h3 id="Literature_on_negative_constraints">Literature on negative constraints</h3></div>

<ul><li><cite id="CITEREFAiken,_A.,_Kozen,_D.,_Wimmers,_E.L.1993" class="citation techreport cs1">Aiken, A., Kozen, D., Wimmers, E.L. (Jun 1993). <a rel="nofollow" class="external text" href="http://theory.stanford.edu/~aiken/publications/papers/ic95.ps">Decidability of Systems of Set Constraints with Negative Constraints</a> (Technical report). Computer Science Department, Cornell University. 93–1362.</cite><code class="cs1-code">{{cite tech report}}</code>: CS1 maint: multiple names: authors list (link)</li>

<li><cite id="CITEREFCharatonik,_W.,_Pacholski,_L.1994" class="citation book cs1">Charatonik, W., Pacholski, L. (Jul 1994). "Negative Set Constraints with Equality". Ninth Annual IEEE Symposium on Logic in Computer Science. pp. 128–136.</cite><code class="cs1-code">{{cite book}}</code>: CS1 maint: multiple names: authors list (link)</li>

<li><cite id="CITEREFR._GilleronS._TisonM._Tommasi1993" class="citation book cs1">R. Gilleron; S. Tison; M. Tommasi (1993). "Solving Systems of Set Constraints with Negated Subset Relationships". Proceedings of the 34th Symp. on Foundations of Computer Science. pp. 372–380.</cite></li>

<li><cite id="CITEREFGilleron,_R.,_Tison,_S.,_Tommasi,_M.1993" class="citation techreport cs1">Gilleron, R., Tison, S., Tommasi, M. (1993). Solving Systems of Set Constraints with Negated Subset Relationships (Technical report). Laboratoire d'Informatique Fondamentale de Lille. IT 247.</cite><code class="cs1-code">{{cite tech report}}</code>: CS1 maint: multiple names: authors list (link)</li>

<li><cite id="CITEREFStefansson,_K.1993" class="citation techreport cs1">Stefansson, K. (Aug 1993). Systems of Set Constraints with Negative Constraints are NEXPTIME-Complete (Technical report). Computer Science Department, Cornell University. 93–1380.</cite></li>

<li><cite id="CITEREFStefansson,_K.1994" class="citation book cs1">Stefansson, K. (1994). "Systems of Set Constraints with Negative Constraints are NEXPTIME-Complete". Ninth Annual IEEE Symposium on Logic in Computer Science. pp. 137–141.</cite></li></ul>

<div class="mw-heading mw-heading2"><h2 id="Notes">Notes</h2></div>

/* start https://en.wikipedia.org/ */

.mw-parser-output .reflist{margin-bottom:0.5em;list-style-type:decimal}@media screen{.mw-parser-output .reflist{font-size:90%}}.mw-parser-output .reflist .references{font-size:100%;margin-bottom:0;list-style-type:inherit}.mw-parser-output .reflist-columns-2{column-width:30em}.mw-parser-output .reflist-columns-3{column-width:25em}.mw-parser-output .reflist-columns{margin-top:0.3em}.mw-parser-output .reflist-columns ol{margin-top:0}.mw-parser-output .reflist-columns li{page-break-inside:avoid;break-inside:avoid-column}.mw-parser-output .reflist-upper-alpha{list-style-type:upper-alpha}.mw-parser-output .reflist-upper-roman{list-style-type:upper-roman}.mw-parser-output .reflist-lower-alpha{list-style-type:lower-alpha}.mw-parser-output .reflist-lower-greek{list-style-type:lower-greek}.mw-parser-output .reflist-lower-roman{list-style-type:lower-roman}

/* end https://en.wikipedia.org/ */

</style><div class="reflist">

<li id="cite_note-1"><a href="#cite_ref-1">^</a> If f is an n-ary function symbol admitted in a term, then "f(E1,...,En)" is a set expression denoting the set { f(t1,...,tn) : t1∈E1 and ... and tn∈En }, where E1,...,En are set expressions in turn.

</li>

<li id="cite_note-2"><a href="#cite_ref-2">^</a> This is similar to describing e.g. a <a href="Rational_number" title="Rational number">rational number</a> as a solution to an equation a⋅x + b = 0, with <a href="Integer" title="Integer">integer</a> coefficients a, b.

</li>

</ol></div></div>

/* start https://en.wikipedia.org/ */

.mw-parser-output .asbox{position:relative;overflow:hidden}.mw-parser-output .asbox table{background:transparent}.mw-parser-output .asbox p{margin:0}.mw-parser-output .asbox p+p{margin-top:0.25em}.mw-parser-output .asbox-body{font-style:italic}.mw-parser-output .asbox-note{font-size:smaller}.mw-parser-output .asbox .navbar{position:absolute;top:-0.75em;right:1em;display:none}.mw-parser-output :not(p):not(.asbox)+style+.asbox,.mw-parser-output :not(p):not(.asbox)+link+.asbox{margin-top:3em}

/* end https://en.wikipedia.org/ */

</style>

</div><div><div class="zim-footer">

This article is issued from <a class="external text" title="Last edited on 2024-11-18" href="https://en.wikipedia.org/wiki/?title=Set_constraint&oldid=1258125781">Wikipedia</a>. The text is available under <a class="external text" href="https://creativecommons.org/licenses/by-sa/4.0/deed.en">Creative Commons Attribution-Share Alike 4.0</a> unless otherwise noted. Additional terms may apply for the media files.

</div>

</div></div>

</div>

</main>

</div>

</body></html>